es:ES, i:Id, L:(IdLnk List), T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 e1@i.
 e2@i.
 n:{0..||"table" when e1|| }, m:{0..||"table" when e2|| }.
 (st-atom("table" when e1;n) = st-atom("table" when e2;m)  Atom1)  (n = m  ) 

latex

Definitions	T, i  j < k, , True, if b then t else f fi , tt, t  T, atoms-distinct(tab), b, P & Q, secret-table(T), "$x", {i..j}, e@i. P(e), P  Q, Id, x:A. B(x), False, A  B, @i(x:T), A, @i only L affect x:T, A c B, , let x = a in b(x), es-secret-server
Lemmas	event system wf, IdLnk wf, es-secret-server wf, es-E wf, Id wf, true wf, squash wf, st-atom wf, le wf, st-length wf, es-loc wf, es-first-unique, data wf, int seg wf, nat wf, secret-table wf, es-vartype wf, es-when wf, ss-table-length, ss-atom-constant, es-first-init, es-loc-init, es-init wf